Inductive Val : Type :=
  | bool_val        : Bool    -> Val
  | int_val         : Integer -> Val
  | byte_val        : Byte    -> Val
  | byte_matrix_val : forall m n, Matrix Byte m n -> Val
.
